googologytestingfandomcom-20200215-history
Buchholz hydra
|image=File:Hydra.jpg |notation=\(\text{BH}(n)\) |author=Wilfried Buchholz |year=1987}} The Buchholz hydra game is a one-player game played on trees labelled with any finite number or \(\omega\). From the game arises a fast-growing function \(\text{BH}(n)\) which eventually dominates all recursive functions provably total in , and is itself provably total in + "the TFB ordinal is well-ordered". Rules The game is played on a finite labelled tree \(T\) where the root is marked with a special label (call it +), and every child of root has label 0, and every other node is labeled by any ordinal \(\leq \omega\). This tree is called a hydra. At each step, we perform a transformation on the tree with two parameters: a leaf node \(a\) and a nonnegative integer \(n\). We alter the hydra using the following rules: # If \(a\) has label 0, we proceed as in Kirby-Paris' game. Call the node's parent \(b\), and its grandparent \(c\) (if it exists). First we delete \(a\). If \(c\) exists (i.e. \(b\) is not the root), we make \(n\) copies of \(b\) and all its children and attach them to \(c\). # If \(a\) has label \(u + 1\), we go down the tree looking for a node \(b\) with label \(v \leq u\) (which is guaranteed to exist, as every child of the root node has label 0). Consider the subtree rooted at \(b\) — call it \(S\). Create a copy of \(S\), call it \(S'\). Within \(S'\), we relabel \(b\) with \(u\) and relabel \(a\) with \(0\). Back in the original tree, replace \(a\) with \(S'\). # If \(a\) has label \(\omega\), we simply relabel it with \(n + 1\). If \(a\) is the hydra's rightmost leaf, we notate the transformed tree as \(T(n)\). As we go about altering the hydra, we pick leaves and values of \(n\). The sequence of leaves and \(n\)'s is called a strategy. A strategy is a winning strategy if it eventually leaves us with only the root node, and a losing strategy otherwise. Hydra theorem Wilfried Buchholz showed that there are no losing strategies for any hydra. Call this the hydra theorem. The hydra theorem is unprovable in , but for individual hydras it is provable. \(\text{BH}(n)\) function Suppose we make a tree with just one branch with \(x\) nodes, labeled \(+,0,\omega,\omega,...,\omega\). Call such a tree \(R^n\). It cannot be proven in that for all \(x\), there exists \(k\) such that \(R^x(1)(2)(3)...(k)\) is root tree. (The latter expression means taking the tree \(R^x\), then transforming it with \(n = 1\), then \(n = 2\), then \(n = 3\), etc. up to \(n = k\).) Define \(\text{BH}(x)\) as the smallest \(k\) such that \(R^x(1)(2)(3)...(k)\) as defined above is root tree. By the hydra theorem this function is well-defined, but its totality cannot be proven in . Its rate of growth is comparable to \(f_{\psi_0(\varepsilon_{\Omega_\omega + 1})}(x)\). (\(\psi_0(\varepsilon_{\Omega_\omega + 1})\) here is the Takeuti-Feferman-Buchholz ordinal, which unsurprisingly measures the strength of .) The first two values of the BH function are virtually degenerate: \(\text{BH}(1) = 0\) and \(\text{BH}(2) = 1\). \(\text{BH}(3)\) is very large, but not extremely — Googology Wiki user provided a heuristic argument for \(\text{BH}(3) < f_{\varepsilon_0}(n)\) for some reasonably small \(n\). The Buchholz hydra surpasses TREE(n) and SCG(n). It is likely weaker than loader.c as well as numbers from finite promise games. Analysis It is possible to make one-to-one correspondence between some hydras and ordinals: Sources and References *W. Buchholz, An independence result for (Π11 - CA) + BI, Ann. Pure Appl. Logic 33 (1987) 131-155. *M. Hamano, M. Okada, A relationship among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game, Math. Logic Quart. 43 (1997) 103-120. *M. Hamano, M. Okada, A direct independence proof of Buchholz's Hydra Game on finite labeled trees, Arch. Math. Logic 37 (1998) 67-89. *L. Kirby, J. Paris, Accessible independence results for Peano Arithmetic, Bull. Lon. Math. Soc. 14 (1982) 285-293. *J. Ketonen, R. Solovay, Rapidly growing Ramsey functions, Ann. Math. 113 (1981) 267-314. *G. Takeuti, Proof Theory, 2nd Edition, North-Holland, Amsterdam, 1987. See also Category:Functions Category:Games Category:Combinatorics